1. $T$ : Type
\\[0ex]2. $E$ : $T$$\rightarrow$$T$$\rightarrow\mathbb{P}$
\\[0ex]3. ($\forall$$a$:$T$. $E$($a$,$a$)) \& ($\forall$$a$, $b$:$T$. $E$($a$,$b$) $\Rightarrow$ $E$($b$,$a$)) \& ($\forall$$a$, $b$, $c$:$T$. $E$($a$,$b$) $\Rightarrow$ $E$($b$,$c$) $\Rightarrow$ $E$($a$,$c$))
\\[0ex]4. $x$ : $T$
\\[0ex]$\vdash$  $E$($x$,$x$)